$\forall$$M$:MsgA, $a$:Knd. $M$.da($a$) $\in$ Type